A,B:es_realizer{i:l}. R-compat{i:l}(A; B)  R-compat{i:l}(B; A) 

latex

Definitions

ge(i; j), False, A, A  B, x. t(x), ff, tt, True, P  Q, if b then t else f fi , Y, prop{i:l}, t  T, R-compat{i:l}(A; B), P  Q, x:A. B(x), , x(s), guard(T), P  Q, P  Q, Unit, , ,

Lemmas

ge wf, nat properties, R-interface-compat wf, R-discrete compat symmetry, R-discrete compat wf, R-frame-compat wf, base-domain-type wf, not functionality wrt iff, Rda wf, Kind-deq wf, Knd wf, Rds wf, id-deq wf, fpf-compatible wf, fpf-compatible-symmetry, assert-eq-bd, R-base-domain wf, eq bd wf, assert-eq-id, Id wf, R-loc wf, eq id wf, true wf, Rnone? wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Rplus-right wf, Rplus-left wf, R-compat-Rplus2, Rplus-implies, R-size-decreases, eqtt to assert, bool wf, Rplus? wf, le wf, es realizer wf, R-compat wf, nat plus wf, R-size wf, nat wf